1  (¬(0≥SUCC0)∧∀N.(¬(N≥SUCCN)⊃¬(SUCCN≥SUCCSUCCN)))⊃∀N.¬(N≥SUCCN)    ∧I (NIL) 

2  ¬(SUCC0=0)    ∀E NIL 0 

3  0≥SUCC0⊃SUCC0=0    ∀E NIL SUCC0 

4  SUCCN≥SUCCSUCCN≡PREDSUCCN≥PREDSUCCSUCCN    ∀E NIL SUCCN , SUCCSUCCN 

5  PREDSUCCN=N    ∀E NIL N 

6  PREDSUCCSUCCN=SUCCN    ∀E NIL SUCCN 

7  SUCCN≥SUCCSUCCN≡N≥PREDSUCCSUCCN    SUBSTR 5 IN 4 

8  SUCCN≥SUCCSUCCN≡N≥SUCCN    SUBSTR 6 IN 7 

9  ¬(N≥SUCCN)⊃¬(SUCCN≥SUCCSUCCN)    TAUT 

10  ∀N.(¬(N≥SUCCN)⊃¬(SUCCN≥SUCCSUCCN))    ∀I 9 N ← N 

11  ∀N.¬(N≥SUCCN)    TAUT 

12  ((¬Q(0,0)∨(Q(0,M*0)∨¬∀I K.((¬(I=0)∧Q(I,K))⊃Q(PREDI,K+M))))∧∀N.((¬Q(N,0)∨(Q(0,M*N)∨¬∀I K.((¬(I=0)∧Q(I,K))⊃Q(P%
REDI,K+M))))⊃(¬Q(SUCCN,0)∨(Q(0,M*SUCCN)∨¬∀I K.((¬(I=0)∧Q(I,K))⊃Q(PREDI,K+M))))))⊃∀N.(¬Q(N,0)∨(Q(0,M*N)∨¬∀I K.((¬%
(I=0)∧Q(I,K))⊃Q(PREDI,K+M))))    ∧I (NIL) 

13  (M*0)=0    ∀E NIL M 

14  ∀N.((¬Q(N,0)∨(Q(0,M*N)∨¬∀I K.((¬(I=0)∧Q(I,K))⊃Q(PREDI,K+M))))⊃(¬Q(SUCCN,0)∨(Q(0,M*SUCCN)∨¬∀I K.((¬(I=0)∧Q(I,%
K))⊃Q(PREDI,K+M)))))⊃∀N.(¬Q(N,0)∨(Q(0,M*N)∨¬∀I K.((¬(I=0)∧Q(I,K))⊃Q(PREDI,K+M))))    TAUTEQ 

15  ∀N.((Q(N,0)∧∀I K.((¬(I=0)∧Q(I,K))⊃Q(PREDI,K+M)))⊃Q(0,M*N))  (15)  ASSUME 

16  (Q(SUCCN,0)∧∀I K.((¬(I=0)∧Q(I,K))⊃Q(PREDI,K+M)))⊃Q(0,M*SUCCN)  (15)  ∀E 15 SUCCN 

17  (¬Q(N,0)∨(Q(0,M*N)∨¬∀I K.((¬(I=0)∧Q(I,K))⊃Q(PREDI,K+M))))⊃(¬Q(SUCCN,0)∨(Q(0,M*SUCCN)∨¬∀I K.((¬(I=0)∧Q(I,K))⊃%
Q(PREDI,K+M))))  (15)  TAUT 

18  ∀N.((¬Q(N,0)∨(Q(0,M*N)∨¬∀I K.((¬(I=0)∧Q(I,K))⊃Q(PREDI,K+M))))⊃(¬Q(SUCCN,0)∨(Q(0,M*SUCCN)∨¬∀I K.((¬(I=0)∧Q(I,%
K))⊃Q(PREDI,K+M)))))  (15)  ∀I 17 N ← N 

19  ∀N.((Q(N,0)∧∀I K.((¬(I=0)∧Q(I,K))⊃Q(PREDI,K+M)))⊃Q(0,M*N))⊃∀N.((¬Q(N,0)∨(Q(0,M*N)∨¬∀I K.((¬(I=0)∧Q(I,K))⊃Q(P%
REDI,K+M))))⊃(¬Q(SUCCN,0)∨(Q(0,M*SUCCN)∨¬∀I K.((¬(I=0)∧Q(I,K))⊃Q(PREDI,K+M)))))    ⊃I 15 18 

20  ∀N.((Q(N,0)∧∀I K.((¬(I=0)∧Q(I,K))⊃Q(PREDI,K+M)))⊃Q(0,M*N))⊃∀N.(¬Q(N,0)∨(Q(0,M*N)∨¬∀I K.((¬(I=0)∧Q(I,K))⊃Q(PR%
EDI,K+M))))    TAUT 

21  Q(N,0)∧∀I K.((¬(I=0)∧Q(I,K))⊃Q(PREDI,K+M))  (21)  ASSUME 

22  Q(N,0)  (21)  TAUT 

23  ∀I K.((¬(I=0)∧Q(I,K))⊃Q(PREDI,K+M))  (21)  TAUT 

24  ((N≥0⊃Q(N-0,M*0))∧∀N1.((N≥N1⊃Q(N-N1,M*N1))⊃(N≥SUCCN1⊃Q(N-SUCCN1,M*SUCCN1))))⊃∀N1.(N≥N1⊃Q(N-N1,M*N1))    ∧I (%
NIL) 

25  (N-0)=N    ∀E NIL N 

26  (M*0)=0    ∀E NIL M 

27  ∀N1.((N≥N1⊃Q(N-N1,M*N1))⊃(N≥SUCCN1⊃Q(N-SUCCN1,M*SUCCN1)))⊃∀N1.(N≥N1⊃Q(N-N1,M*N1))  (21)  TAUTEQ 

28  N≥N1⊃Q(N-N1,M*N1)  (28)  ASSUME 

29  NATNUM(N-N1)⊃((¬((N-N1)=0)∧Q(N-N1,M*N1))⊃Q(PRED(N-N1),(M*N1)+M))  (21)  ∀E 23 N-N1 , M*N1 

30  N≥SUCCN1  (30)  ASSUME 

31  N≥SUCCN1⊃N≥N1    ∀E NIL N , N1 

32  N≥SUCCN1⊃¬((N-N1)=0)    ∀E NIL N , N1 

33  N≥N1⊃NATNUM(N-N1)    ∀E NIL N , N1 

34  Q(PRED(N-N1),(M*N1)+M)  (21 28 30)  TAUT 

35  N≥SUCCN1⊃Q(PRED(N-N1),(M*N1)+M)  (21 28)  ⊃I 30 34 

36  (N≥N1⊃Q(N-N1,M*N1))⊃(N≥SUCCN1⊃Q(PRED(N-N1),(M*N1)+M))  (21)  ⊃I 28 35 

37  (M*SUCCN1)=((M*N1)+M)    ∀E NIL M , N1 

38  (N≥N1⊃Q(N-N1,M*N1))⊃(N≥SUCCN1⊃Q(PRED(N-N1),M*SUCCN1))  (21)  SUBST 37 IN 36 

39  (N-SUCCN1)=PRED(N-N1)    ∀E NIL N , N1 

40  (N≥N1⊃Q(N-N1,M*N1))⊃(N≥SUCCN1⊃Q(N-SUCCN1,M*SUCCN1))  (21)  SUBST 39 IN 38 

41  ∀N1.((N≥N1⊃Q(N-N1,M*N1))⊃(N≥SUCCN1⊃Q(N-SUCCN1,M*SUCCN1)))  (21)  ∀I 40 N1 ← N1 

42  ∀N1.(N≥N1⊃Q(N-N1,M*N1))  (21)  ⊃E 27 41 

43  N≥N⊃Q(N-N,M*N)  (21)  ∀E 42 N 

44  (N-N)=0    ∀E NIL N 

45  N≥N⊃Q(0,M*N)  (21)  SUBSTR 44 IN 43 

46  N≥N    ∀E NIL N 

47  Q(0,M*N)  (21)  ⊃E 46 45 

48  (Q(N,0)∧∀I K.((¬(I=0)∧Q(I,K))⊃Q(PREDI,K+M)))⊃Q(0,M*N)    ⊃I 21 47 

49  ∀N.((Q(N,0)∧∀I K.((¬(I=0)∧Q(I,K))⊃Q(PREDI,K+M)))⊃Q(0,M*N))    ∀I 48 N ← N 

50  ∀N.(¬Q(N,0)∨(Q(0,M*N)∨¬∀I K.((¬(I=0)∧Q(I,K))⊃Q(PREDI,K+M))))    ⊃E 49 20